The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

inc(s(x)) → s(inc(x)) [1]
inc(0) → s(0) [1]
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x)) [1]
ifPlus(false, x, y, z) → plus(x, z) [1]
ifPlus(true, x, y, z) → y [1]
minus(s(x), s(y)) → minus(x, y) [1]
minus(0, x) → 0 [1]
minus(x, 0) → x [1]
minus(x, x) → 0 [1]
eq(s(x), s(y)) → eq(x, y) [1]
eq(0, s(x)) → false [1]
eq(s(x), 0) → false [1]
eq(0, 0) → true [1]
eq(x, x) → true [1]
times(x, y) → timesIter(x, y, 0) [1]
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z)) [1]
ifTimes(true, x, y, z, u) → z [1]
ifTimes(false, x, y, z, u) → timesIter(x, y, u) [1]
f → g [1]
f → h [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

inc(s(x)) → s(inc(x)) [1]
inc(0) → s(0) [1]
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x)) [1]
ifPlus(false, x, y, z) → plus(x, z) [1]
ifPlus(true, x, y, z) → y [1]
minus(s(x), s(y)) → minus(x, y) [1]
minus(0, x) → 0 [1]
minus(x, 0) → x [1]
minus(x, x) → 0 [1]
eq(s(x), s(y)) → eq(x, y) [1]
eq(0, s(x)) → false [1]
eq(s(x), 0) → false [1]
eq(0, 0) → true [1]
eq(x, x) → true [1]
times(x, y) → timesIter(x, y, 0) [1]
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z)) [1]
ifTimes(true, x, y, z, u) → z [1]
ifTimes(false, x, y, z, u) → timesIter(x, y, u) [1]
f → g [1]
f → h [1]

The TRS has the following type information:

inc :: s:0 → s:0 s :: s:0 → s:0 0 :: s:0 plus :: s:0 → s:0 → s:0 ifPlus :: false:true → s:0 → s:0 → s:0 → s:0 eq :: s:0 → s:0 → false:true minus :: s:0 → s:0 → s:0 false :: false:true true :: false:true times :: s:0 → s:0 → s:0 timesIter :: s:0 → s:0 → s:0 → s:0 ifTimes :: false:true → s:0 → s:0 → s:0 → s:0 → s:0 f :: g:h g :: g:h h :: g:h

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:
none

And the following fresh constants: none

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: inc(s(x)) → s(inc(x)) [1] inc(0) → s(0) [1] plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x)) [1] ifPlus(false, x, y, z) → plus(x, z) [1] ifPlus(true, x, y, z) → y [1] minus(s(x), s(y)) → minus(x, y) [1] minus(0, x) → 0 [1] minus(x, 0) → x [1] minus(x, x) → 0 [1] eq(s(x), s(y)) → eq(x, y) [1] eq(0, s(x)) → false [1] eq(s(x), 0) → false [1] eq(0, 0) → true [1] eq(x, x) → true [1] times(x, y) → timesIter(x, y, 0) [1] timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z)) [1] ifTimes(true, x, y, z, u) → z [1] ifTimes(false, x, y, z, u) → timesIter(x, y, u) [1] f → g [1] f → h [1] The TRS has the following type information: inc :: s:0 → s:0 s :: s:0 → s:0 0 :: s:0 plus :: s:0 → s:0 → s:0 ifPlus :: false:true → s:0 → s:0 → s:0 → s:0 eq :: s:0 → s:0 → false:true minus :: s:0 → s:0 → s:0 false :: false:true true :: false:true times :: s:0 → s:0 → s:0 timesIter :: s:0 → s:0 → s:0 → s:0 ifTimes :: false:true → s:0 → s:0 → s:0 → s:0 → s:0 f :: g:h g :: g:h h :: g:h Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
false => 0
true => 1
g => 0
h => 1

(8) Obligation:

Complexity RNTS consisting of the following rules:

eq(z', z'') -{ 1 }→ eq(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 1 :|: z' = x, x >= 0, z'' = x
eq(z', z'') -{ 1 }→ 0 :|: x >= 0, z'' = 1 + x, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' = 1 + x, x >= 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
ifPlus(z', z'', z1, z2) -{ 1 }→ y :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1
ifPlus(z', z'', z1, z2) -{ 1 }→ plus(x, z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ z :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1, z3 = u, u >= 0
ifTimes(z', z'', z1, z2, z3) -{ 1 }→ timesIter(x, y, u) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z3 = u, z' = 0, u >= 0
inc(z') -{ 1 }→ 1 + inc(x) :|: z' = 1 + x, x >= 0
inc(z') -{ 1 }→ 1 + 0 :|: z' = 0
minus(z', z'') -{ 1 }→ x :|: z'' = 0, z' = x, x >= 0
minus(z', z'') -{ 1 }→ minus(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
minus(z', z'') -{ 1 }→ 0 :|: x >= 0, z'' = x, z' = 0
minus(z', z'') -{ 1 }→ 0 :|: z' = x, x >= 0, z'' = x
plus(z', z'') -{ 1 }→ ifPlus(eq(x, 0), minus(x, 1 + 0), x, inc(x)) :|: z' = x, z'' = y, x >= 0, y >= 0
times(z', z'') -{ 1 }→ timesIter(x, y, 0) :|: z' = x, z'' = y, x >= 0, y >= 0
timesIter(z', z'', z1) -{ 1 }→ ifTimes(eq(x, 0), minus(x, 1 + 0), y, z, plus(y, z)) :|: z1 = z, z >= 0, z' = x, z'' = y, x >= 0, y >= 0

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V2, V5, V6, V28),0,[inc(V, Out)],[V >= 0]). eq(start(V, V2, V5, V6, V28),0,[plus(V, V2, Out)],[V >= 0,V2 >= 0]). eq(start(V, V2, V5, V6, V28),0,[ifPlus(V, V2, V5, V6, Out)],[V >= 0,V2 >= 0,V5 >= 0,V6 >= 0]). eq(start(V, V2, V5, V6, V28),0,[minus(V, V2, Out)],[V >= 0,V2 >= 0]). eq(start(V, V2, V5, V6, V28),0,[eq(V, V2, Out)],[V >= 0,V2 >= 0]). eq(start(V, V2, V5, V6, V28),0,[times(V, V2, Out)],[V >= 0,V2 >= 0]). eq(start(V, V2, V5, V6, V28),0,[timesIter(V, V2, V5, Out)],[V >= 0,V2 >= 0,V5 >= 0]). eq(start(V, V2, V5, V6, V28),0,[ifTimes(V, V2, V5, V6, V28, Out)],[V >= 0,V2 >= 0,V5 >= 0,V6 >= 0,V28 >= 0]). eq(start(V, V2, V5, V6, V28),0,[f(Out)],[]). eq(inc(V, Out),1,[inc(V1, Ret1)],[Out = 1 + Ret1,V = 1 + V1,V1 >= 0]). eq(inc(V, Out),1,[],[Out = 1,V = 0]). eq(plus(V, V2, Out),1,[eq(V3, 0, Ret0),minus(V3, 1 + 0, Ret11),inc(V3, Ret3),ifPlus(Ret0, Ret11, V3, Ret3, Ret)],[Out = Ret,V = V3,V2 = V4,V3 >= 0,V4 >= 0]). eq(ifPlus(V, V2, V5, V6, Out),1,[plus(V7, V8, Ret2)],[Out = Ret2,V5 = V9,V8 >= 0,V6 = V8,V7 >= 0,V9 >= 0,V2 = V7,V = 0]). eq(ifPlus(V, V2, V5, V6, Out),1,[],[Out = V10,V5 = V10,V11 >= 0,V6 = V11,V12 >= 0,V10 >= 0,V2 = V12,V = 1]). eq(minus(V, V2, Out),1,[minus(V13, V14, Ret4)],[Out = Ret4,V = 1 + V13,V13 >= 0,V14 >= 0,V2 = 1 + V14]). eq(minus(V, V2, Out),1,[],[Out = 0,V15 >= 0,V2 = V15,V = 0]). eq(minus(V, V2, Out),1,[],[Out = V16,V2 = 0,V = V16,V16 >= 0]). eq(minus(V, V2, Out),1,[],[Out = 0,V = V17,V17 >= 0,V2 = V17]). eq(eq(V, V2, Out),1,[eq(V18, V19, Ret5)],[Out = Ret5,V = 1 + V18,V18 >= 0,V19 >= 0,V2 = 1 + V19]). eq(eq(V, V2, Out),1,[],[Out = 0,V20 >= 0,V2 = 1 + V20,V = 0]). eq(eq(V, V2, Out),1,[],[Out = 0,V2 = 0,V = 1 + V21,V21 >= 0]). eq(eq(V, V2, Out),1,[],[Out = 1,V2 = 0,V = 0]). eq(eq(V, V2, Out),1,[],[Out = 1,V = V22,V22 >= 0,V2 = V22]). eq(times(V, V2, Out),1,[timesIter(V23, V24, 0, Ret6)],[Out = Ret6,V = V23,V2 = V24,V23 >= 0,V24 >= 0]). eq(timesIter(V, V2, V5, Out),1,[eq(V25, 0, Ret01),minus(V25, 1 + 0, Ret12),plus(V26, V27, Ret41),ifTimes(Ret01, Ret12, V26, V27, Ret41, Ret7)],[Out = Ret7,V5 = V27,V27 >= 0,V = V25,V2 = V26,V25 >= 0,V26 >= 0]). eq(ifTimes(V, V2, V5, V6, V28, Out),1,[],[Out = V29,V5 = V30,V29 >= 0,V6 = V29,V31 >= 0,V30 >= 0,V2 = V31,V = 1,V28 = V32,V32 >= 0]). eq(ifTimes(V, V2, V5, V6, V28, Out),1,[timesIter(V33, V34, V35, Ret8)],[Out = Ret8,V5 = V34,V36 >= 0,V6 = V36,V33 >= 0,V34 >= 0,V2 = V33,V28 = V35,V = 0,V35 >= 0]). eq(f(Out),1,[],[Out = 0]). eq(f(Out),1,[],[Out = 1]). input_output_vars(inc(V,Out),[V],[Out]). input_output_vars(plus(V,V2,Out),[V,V2],[Out]). input_output_vars(ifPlus(V,V2,V5,V6,Out),[V,V2,V5,V6],[Out]). input_output_vars(minus(V,V2,Out),[V,V2],[Out]). input_output_vars(eq(V,V2,Out),[V,V2],[Out]). input_output_vars(times(V,V2,Out),[V,V2],[Out]). input_output_vars(timesIter(V,V2,V5,Out),[V,V2,V5],[Out]). input_output_vars(ifTimes(V,V2,V5,V6,V28,Out),[V,V2,V5,V6,V28],[Out]). input_output_vars(f(Out),[],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. recursive : [eq/3]
1. non_recursive : [f/1]
2. recursive : [inc/2]
3. recursive : [minus/3]
4. recursive : [ifPlus/5,plus/3]
5. recursive : [ifTimes/6,timesIter/4]
6. non_recursive : [times/3]
7. non_recursive : [start/5]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into eq/3
1. SCC is partially evaluated into f/1
2. SCC is partially evaluated into inc/2
3. SCC is partially evaluated into minus/3
4. SCC is partially evaluated into plus/3
5. SCC is partially evaluated into timesIter/4
6. SCC is completely evaluated into other SCCs
7. SCC is partially evaluated into start/5

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations eq/3
* CE 25 is refined into CE [28]
* CE 24 is refined into CE [29]
* CE 23 is refined into CE [30]
* CE 22 is refined into CE [31]


### Cost equations --> "Loop" of eq/3
* CEs [31] --> Loop 18
* CEs [28] --> Loop 19
* CEs [29] --> Loop 20
* CEs [30] --> Loop 21

### Ranking functions of CR eq(V,V2,Out)
* RF of phase [18]: [V,V2]

#### Partial ranking functions of CR eq(V,V2,Out)
* Partial RF of phase [18]:
- RF of loop [18:1]:
V
V2


### Specialization of cost equations f/1
* CE 27 is refined into CE [32]
* CE 26 is refined into CE [33]


### Cost equations --> "Loop" of f/1
* CEs [32] --> Loop 22
* CEs [33] --> Loop 23

### Ranking functions of CR f(Out)

#### Partial ranking functions of CR f(Out)


### Specialization of cost equations inc/2
* CE 17 is refined into CE [34]
* CE 16 is refined into CE [35]


### Cost equations --> "Loop" of inc/2
* CEs [35] --> Loop 24
* CEs [34] --> Loop 25

### Ranking functions of CR inc(V,Out)
* RF of phase [24]: [V]

#### Partial ranking functions of CR inc(V,Out)
* Partial RF of phase [24]:
- RF of loop [24:1]:
V


### Specialization of cost equations minus/3
* CE 21 is refined into CE [36]
* CE 20 is refined into CE [37]
* CE 19 is refined into CE [38]
* CE 18 is refined into CE [39]


### Cost equations --> "Loop" of minus/3
* CEs [39] --> Loop 26
* CEs [36] --> Loop 27
* CEs [37] --> Loop 28
* CEs [38] --> Loop 29

### Ranking functions of CR minus(V,V2,Out)
* RF of phase [26]: [V,V2]

#### Partial ranking functions of CR minus(V,V2,Out)
* Partial RF of phase [26]:
- RF of loop [26:1]:
V
V2


### Specialization of cost equations plus/3
* CE 15 is refined into CE [40,41,42]
* CE 14 is refined into CE [43]


### Cost equations --> "Loop" of plus/3
* CEs [43] --> Loop 30
* CEs [40,41,42] --> Loop 31

### Ranking functions of CR plus(V,V2,Out)
* RF of phase [31]: [V]

#### Partial ranking functions of CR plus(V,V2,Out)
* Partial RF of phase [31]:
- RF of loop [31:1]:
V


### Specialization of cost equations timesIter/4
* CE 13 is refined into CE [44,45]
* CE 12 is refined into CE [46,47,48,49,50,51]


### Cost equations --> "Loop" of timesIter/4
* CEs [47,49,51] --> Loop 32
* CEs [46,48,50] --> Loop 33
* CEs [45] --> Loop 34
* CEs [44] --> Loop 35

### Ranking functions of CR timesIter(V,V2,V5,Out)
* RF of phase [32]: [V]
* RF of phase [33]: [V]

#### Partial ranking functions of CR timesIter(V,V2,V5,Out)
* Partial RF of phase [32]:
- RF of loop [32:1]:
V
* Partial RF of phase [33]:
- RF of loop [33:1]:
V


### Specialization of cost equations start/5
* CE 2 is refined into CE [52,53,54,55]
* CE 3 is refined into CE [56]
* CE 4 is refined into CE [57,58]
* CE 5 is refined into CE [59,60]
* CE 6 is refined into CE [61,62]
* CE 7 is refined into CE [63,64,65,66,67]
* CE 8 is refined into CE [68,69,70,71,72]
* CE 9 is refined into CE [73,74,75,76]
* CE 10 is refined into CE [77,78,79,80]
* CE 11 is refined into CE [81,82]


### Cost equations --> "Loop" of start/5
* CEs [52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82] --> Loop 36

### Ranking functions of CR start(V,V2,V5,V6,V28)

#### Partial ranking functions of CR start(V,V2,V5,V6,V28)


Computing Bounds
=====================================

#### Cost of chains of eq(V,V2,Out):
* Chain [[18],21]: 1*it(18)+1
Such that:it(18) =< V

with precondition: [Out=0,V>=1,V2>=V+1]

* Chain [[18],20]: 1*it(18)+1
Such that:it(18) =< V2

with precondition: [Out=0,V2>=1,V>=V2+1]

* Chain [[18],19]: 1*it(18)+1
Such that:it(18) =< V

with precondition: [Out=1,V=V2,V>=1]

* Chain [21]: 1
with precondition: [V=0,Out=0,V2>=1]

* Chain [20]: 1
with precondition: [V2=0,Out=0,V>=1]

* Chain [19]: 1
with precondition: [Out=1,V2=V,V2>=0]


#### Cost of chains of f(Out):
* Chain [23]: 1
with precondition: [Out=0]

* Chain [22]: 1
with precondition: [Out=1]


#### Cost of chains of inc(V,Out):
* Chain [[24],25]: 1*it(24)+1
Such that:it(24) =< Out

with precondition: [V+1=Out,V>=1]

* Chain [25]: 1
with precondition: [V=0,Out=1]


#### Cost of chains of minus(V,V2,Out):
* Chain [[26],29]: 1*it(26)+1
Such that:it(26) =< V

with precondition: [Out=0,V>=1,V2>=V]

* Chain [[26],28]: 1*it(26)+1
Such that:it(26) =< V2

with precondition: [V=Out+V2,V2>=1,V>=V2]

* Chain [[26],27]: 1*it(26)+1
Such that:it(26) =< V

with precondition: [Out=0,V=V2,V>=1]

* Chain [29]: 1
with precondition: [V=0,Out=0,V2>=0]

* Chain [28]: 1
with precondition: [V2=0,V=Out,V>=0]

* Chain [27]: 1
with precondition: [Out=0,V2=V,V2>=0]


#### Cost of chains of plus(V,V2,Out):
* Chain [[31],30]: 8*it(31)+2*s(16)+1*s(17)+5
Such that:aux(5) =< V+1
aux(8) =< V
it(31) =< aux(8)
s(17) =< it(31)*aux(5)
s(18) =< aux(8)*2
s(16) =< s(18)

with precondition: [Out=0,V>=1,V2>=0]

* Chain [30]: 5
with precondition: [V=0,Out=0,V2>=0]


#### Cost of chains of timesIter(V,V2,V5,Out):
* Chain [[33],35]: 12*it(33)+9
Such that:it(33) =< V

with precondition: [V2=0,Out=0,V>=1,V5>=0]

* Chain [[32],34]: 12*it(32)+8*s(27)+1*s(28)+2*s(30)+24*s(61)+3*s(62)+6*s(63)+9
Such that:s(26) =< V2
aux(17) =< V
aux(18) =< V2+1
s(27) =< s(26)
s(28) =< s(27)*aux(18)
s(29) =< s(26)*2
s(30) =< s(29)
it(32) =< aux(17)
aux(14) =< aux(18)-1
s(65) =< it(32)*aux(14)
s(61) =< s(65)
s(62) =< s(61)*aux(18)
s(64) =< s(65)*2
s(63) =< s(64)

with precondition: [Out=0,V>=1,V2>=1,V5>=0]

* Chain [35]: 9
with precondition: [V=0,V2=0,V5=Out,V5>=0]

* Chain [34]: 8*s(27)+1*s(28)+2*s(30)+9
Such that:s(26) =< V2
s(25) =< V2+1
s(27) =< s(26)
s(28) =< s(27)*s(25)
s(29) =< s(26)*2
s(30) =< s(29)

with precondition: [V=0,V5=Out,V2>=1,V5>=0]


#### Cost of chains of start(V,V2,V5,V6,V28):
* Chain [36]: 16*s(69)+2*s(70)+4*s(72)+66*s(73)+24*s(84)+3*s(85)+6*s(87)+5*s(91)+10*s(93)+1*s(94)+60*s(97)+1*s(98)+2*s(100)+48*s(124)+6*s(125)+12*s(127)+10
Such that:aux(19) =< V
aux(20) =< V+1
aux(21) =< V2
aux(22) =< V2+1
aux(23) =< V5
aux(24) =< V5+1
s(97) =< aux(19)
s(94) =< aux(20)
s(73) =< aux(21)
s(98) =< s(97)*aux(20)
s(99) =< aux(19)*2
s(100) =< s(99)
s(91) =< s(73)*aux(22)
s(92) =< aux(21)*2
s(93) =< s(92)
s(122) =< aux(22)-1
s(123) =< s(97)*s(122)
s(124) =< s(123)
s(125) =< s(124)*aux(22)
s(126) =< s(123)*2
s(127) =< s(126)
s(69) =< aux(23)
s(70) =< s(69)*aux(24)
s(71) =< aux(23)*2
s(72) =< s(71)
s(82) =< aux(24)-1
s(83) =< s(73)*s(82)
s(84) =< s(83)
s(85) =< s(84)*aux(24)
s(86) =< s(83)*2
s(87) =< s(86)

with precondition: []


Closed-form bounds of start(V,V2,V5,V6,V28):
-------------------------------------
* Chain [36] with precondition: []
- Upper bound: nat(V)*64+10+nat(V2)*86+nat(V5)*24+nat(nat(V2+1)+ -1)*72*nat(V)+nat(nat(V5+1)+ -1)*36*nat(V2)+nat(V+1)+nat(V+1)*nat(V)+nat(V2+1)*5*nat(V2)+nat(V2+1)*6*nat(nat(V2+1)+ -1)*nat(V)+nat(V5+1)*2*nat(V5)+nat(V5+1)*3*nat(nat(V5+1)+ -1)*nat(V2)
- Complexity: n^3

### Maximum cost of start(V,V2,V5,V6,V28): nat(V)*64+10+nat(V2)*86+nat(V5)*24+nat(nat(V2+1)+ -1)*72*nat(V)+nat(nat(V5+1)+ -1)*36*nat(V2)+nat(V+1)+nat(V+1)*nat(V)+nat(V2+1)*5*nat(V2)+nat(V2+1)*6*nat(nat(V2+1)+ -1)*nat(V)+nat(V5+1)*2*nat(V5)+nat(V5+1)*3*nat(nat(V5+1)+ -1)*nat(V2)
Asymptotic class: n^3
* Total analysis performed in 512 ms.

(10) BOUNDS(1, n^3)